%%%% Framed ITL

a0(X):- length(5),
	frame(X,(X=a,[](write(X)))).

%          same as X = a, stable(X) 
%          generates sequence  a a a a a

a1(X):- length(5),
	frame(X,(X=1, <>(X:= X+1), [](write(X)))).

%          same as X=1,stable(X) & skip,@X=X+1 & stable(X).  
%          generates sequence  1 2 2 2 2

a2(X):- length(5),
	frame(X,(X=1,(readonly(X)  ,  <>( X:= X+1)),[](write(X)))).

%          This is false

a3(X):- length(5),
	frame(X,(X=1,(readonly(X)  // <>( X:= X+1)),[](write(X)))).

%          same as X=1,stable(X) & skip,@X=X+1 & stable(X).
%          generates sequence  1 2 2 2 2

a4(X):- length(5),
	frame(X,(X=1,(<>(X:=f(X))  // <>( X:= g(X))),[](write(X)))).

%          non deterministic assignments, result may either f(g(1) g(f(1))
%          generates sequence  1 f(1) g(f(1) g(f(1) g(f(1))
%     (non deterministic executions are simulated by backtrack)

a5(X):- length(5),
	frame(X,(readonly(X),
		(X=1,(<>(X:=f(X))  // <>( X:= g(X))),[](write(X))))).
% This fails why? See process group and process id
a6(X):- length(5),
	frame(X,([](ppid(P)),[](write(P)),
		(X=1,
		(<>(X:=f(X)),   [](ppid(P0)),[](write(P0))
		// 		[](ppid(P1)),[](write(P1)),
		 <>( X:= g(X)), [](flag(X,F)),[](write([F])))
		 ,[](write([X]))))).

frtest :- a2(_).
frtest :- write('a2 fail'),nl,@fail.
frtest :- a5(_).
frtest :- write('a5 fail'),nl,@fail.
frtest :- a0(_) & @
	a1(_) & @
	a3(_) & @
	a4(_) & @
	a6(_).
